\section{Conclusion}
\label{sec.concl}

The Maude Formal Environment is
an executable and highly extensible software infrastructure written in Maude
within which a user can interact with several 
tools to mechanically verify properties of Maude specifications.
MFE exploits Maude as a reflective declarative language and system based on 
rewriting logic in which computation corresponds to efficient deduction by rewriting.
We have explained the main design decisions in MFE and integrated, as a proof
of concept, five important formal analysis tools with highly heterogeneous designs: 
namely, Maude's Termination Tool, Church-Rosser Checker, Coherence Checker, Sufficient 
Completeness Checker, and Inductive Theorem Prover.
We also presented a brief overview of 
the steps underwent to integrate Maude's SCC in MFE and explained
how MFE's design decisions allowed for an easy integration. 
It is important to highlight that the approach taken here for extending MFE with the SCC
is one of many possible ways to benefit from the software infrastructure offered by MFE.
Finally, we gave a fair overview of some of the features and commands of 
MFE on the classical example of the readers and writers.

Much work remains ahead. First of all, more tools such as Maude's LTL and LTLR Model Checkers,
Maude's Invariant Analyzer Tool, and Real-Time Maude could be integrated in MFE.
This will result in a more interesting environment with features for handling
broader applications with less effort for the user. One could also think of handling proof obligations such as those for the protecting and extending importations of modules, for the instantiation of parameterized modules, or simply the termination and Church-Rosser assumptions for equational simplification. More ambitiously, a graphical
user interface and support for better interoperability will enhance the
user experience with the formal environment. The graphical user interface could be
developed, for instance, as a plugin in the Eclipse environment. 
IMaude and the IOP platform might also be a good candidates for improving 
tool interoperability and providing the environment with a graphical user interface.

\paragraph{\bf Acknowledgements.} The authors would like to thank the anonymous
referees for comments that helped to improved the paper. 
The first author has been partially supported by 
Spanish Research Projects TIN2008-03107 and P07-TIC-03184.
The second author has been partially supported by 
NSF grants CNS 07-16638 and CCF 09-05584.
%The third author has been partially supported by 
%grants WWW and ZZZ. 
